/* Benchmarks for the PionterC verifier. */

// list insert

struct list
{
  int data;
  struct list* next;
};

/*@ */
struct list* insert_list1(struct list* l, int d)
{
  struct list* temp;
  
  // malloc a new list node and initialize it
  temp = alloc(struct list);
  temp->data = d;
  temp->next = null;
  if (null==l)
    return temp;
  else
  {
    temp->next = l;
    return temp;
  }
}
/*@  result!=null */


/*@ Pi={{l}}*/
struct list* insert_list2(struct list* l, int d)
{
  struct list* temp;
  
  // malloc a new list node and initialize it
  temp = alloc(struct list);
  temp->data = d;
  temp->next = l;
  return temp;
}
/*@  result!=null */
